\begin{tabbing}
$\forall$$i$, $x$:Id, $k$:Knd, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $T$:Type, $f$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$${\it ds}$($x$)?Void).
\\[0ex](isrcv($k$) $\Rightarrow$ $i$ $=$ destination(lnk($k$)))
\\[0ex]$\Rightarrow$ \=@$i$: with declarations \+
\\[0ex]ds:${\it ds}$
\\[0ex]da:$k$ : $T$
\\[0ex]
\\[0ex]effect of $k$(v) is $x$ := $f$ s v 
\\[0ex]realizes ${\it es}$.
\\[0ex]@$i$ events of kind $k$ change $x$ to $f$ State(${\it ds}$) (val:$T$)
\-
\end{tabbing}